(1
 (
  ("(var3 stable)" 0 92)
  ("(var3 down)" 92 95)
  ("(var3 up)" 95 124)
  ("(var3 stable)" 124 373)
  ("(var4 stable)" 0 94)
  ("(var4 up)" 94 96)
  ("(var4 stable)" 96 98)
  ("(var4 up)" 98 127)
  ("(var4 stable)" 127 373)
  ("(var1 stable)" 0 89)
  ("(var1 up)" 89 128)
  ("(var1 stable)" 128 373)
  ("(var2 stable)" 0 109)
  ("(var2 up)" 109 113)
  ("(var2 down)" 113 116)
  ("(var2 up)" 116 269)
  ("(var2 stable)" 269 373)
 )
)
(2
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 90)
  ("(var3 stable)" 90 334)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 60)
  ("(var4 up)" 60 94)
  ("(var4 stable)" 94 334)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 94)
  ("(var1 stable)" 94 334)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 stable)" 84 127)
  ("(var2 up)" 127 218)
  ("(var2 stable)" 218 334)
 )
)
(3
 (
  ("(var3 stable)" 0 62)
  ("(var3 up)" 62 99)
  ("(var3 stable)" 99 335)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 98)
  ("(var4 stable)" 98 335)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 85)
  ("(var1 stable)" 85 87)
  ("(var1 up)" 87 92)
  ("(var1 stable)" 92 335)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 84)
  ("(var2 down)" 84 87)
  ("(var2 up)" 87 241)
  ("(var2 stable)" 241 333)
  ("(var2 down)" 333 335)
 )
)
(4
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 81)
  ("(var3 stable)" 81 322)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 48)
  ("(var4 up)" 48 77)
  ("(var4 stable)" 77 322)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 75)
  ("(var1 stable)" 75 322)
  ("(var2 stable)" 0 63)
  ("(var2 up)" 63 65)
  ("(var2 down)" 65 70)
  ("(var2 up)" 70 196)
  ("(var2 stable)" 196 322)
 )
)
(5
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 109)
  ("(var3 stable)" 109 112)
  ("(var3 up)" 112 114)
  ("(var3 stable)" 114 354)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 84)
  ("(var4 stable)" 84 86)
  ("(var4 up)" 86 106)
  ("(var4 stable)" 106 354)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 105)
  ("(var1 stable)" 105 354)
  ("(var2 stable)" 0 92)
  ("(var2 up)" 92 94)
  ("(var2 down)" 94 99)
  ("(var2 stable)" 99 143)
  ("(var2 up)" 143 241)
  ("(var2 stable)" 241 354)
 )
)
(6
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 76)
  ("(var3 down)" 76 78)
  ("(var3 stable)" 78 327)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 77)
  ("(var4 stable)" 77 327)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 50)
  ("(var1 up)" 50 52)
  ("(var1 down)" 52 54)
  ("(var1 up)" 54 70)
  ("(var1 down)" 70 72)
  ("(var1 up)" 72 74)
  ("(var1 down)" 74 76)
  ("(var1 stable)" 76 327)
  ("(var2 stable)" 0 61)
  ("(var2 up)" 61 63)
  ("(var2 down)" 63 68)
  ("(var2 up)" 68 183)
  ("(var2 stable)" 183 327)
 )
)
(7
 (
  ("(var3 stable)" 0 48)
  ("(var3 up)" 48 50)
  ("(var3 stable)" 50 52)
  ("(var3 up)" 52 77)
  ("(var3 stable)" 77 328)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 47)
  ("(var4 stable)" 47 50)
  ("(var4 up)" 50 80)
  ("(var4 down)" 80 82)
  ("(var4 up)" 82 86)
  ("(var4 stable)" 86 328)
  ("(var1 stable)" 0 50)
  ("(var1 up)" 50 52)
  ("(var1 down)" 52 54)
  ("(var1 up)" 54 78)
  ("(var1 stable)" 78 328)
  ("(var2 stable)" 0 63)
  ("(var2 up)" 63 65)
  ("(var2 down)" 65 70)
  ("(var2 up)" 70 182)
  ("(var2 stable)" 182 328)
 )
)
(8
 (
  ("(var3 stable)" 0 29)
  ("(var3 up)" 29 53)
  ("(var3 stable)" 53 267)
  ("(var4 stable)" 0 28)
  ("(var4 down)" 28 30)
  ("(var4 up)" 30 50)
  ("(var4 stable)" 50 267)
  ("(var1 stable)" 0 32)
  ("(var1 up)" 32 48)
  ("(var1 down)" 48 51)
  ("(var1 stable)" 51 267)
  ("(var2 stable)" 0 40)
  ("(var2 up)" 40 42)
  ("(var2 down)" 42 47)
  ("(var2 stable)" 47 69)
  ("(var2 up)" 69 159)
  ("(var2 stable)" 159 267)
 )
)
(9
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 128)
  ("(var3 stable)" 128 368)
  ("(var4 stable)" 0 97)
  ("(var4 up)" 97 129)
  ("(var4 stable)" 129 368)
  ("(var1 stable)" 0 97)
  ("(var1 up)" 97 123)
  ("(var1 stable)" 123 368)
  ("(var2 stable)" 0 110)
  ("(var2 up)" 110 114)
  ("(var2 down)" 114 117)
  ("(var2 up)" 117 266)
  ("(var2 stable)" 266 368)
 )
)
(10
 (
  ("(var3 stable)" 0 92)
  ("(var3 up)" 92 123)
  ("(var3 stable)" 123 372)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 89)
  ("(var4 stable)" 89 95)
  ("(var4 up)" 95 125)
  ("(var4 stable)" 125 372)
  ("(var1 stable)" 0 95)
  ("(var1 up)" 95 117)
  ("(var1 stable)" 117 372)
  ("(var2 stable)" 0 106)
  ("(var2 up)" 106 110)
  ("(var2 down)" 110 113)
  ("(var2 up)" 113 269)
  ("(var2 stable)" 269 372)
 )
)
(11
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 68)
  ("(var3 stable)" 68 305)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 70)
  ("(var4 stable)" 70 305)
  ("(var1 stable)" 0 36)
  ("(var1 up)" 36 66)
  ("(var1 stable)" 66 305)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 56)
  ("(var2 down)" 56 61)
  ("(var2 up)" 61 185)
  ("(var2 stable)" 185 305)
 )
)
(12
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 104)
  ("(var3 stable)" 104 336)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 104)
  ("(var4 stable)" 104 336)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 103)
  ("(var1 down)" 103 105)
  ("(var1 up)" 105 107)
  ("(var1 stable)" 107 336)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 90)
  ("(var2 down)" 90 95)
  ("(var2 stable)" 95 136)
  ("(var2 up)" 136 217)
  ("(var2 stable)" 217 336)
 )
)
(13
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 97)
  ("(var3 stable)" 97 324)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 63)
  ("(var4 stable)" 63 65)
  ("(var4 up)" 65 90)
  ("(var4 stable)" 90 324)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 65)
  ("(var1 down)" 65 67)
  ("(var1 up)" 67 88)
  ("(var1 stable)" 88 324)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 78)
  ("(var2 down)" 78 83)
  ("(var2 up)" 83 204)
  ("(var2 stable)" 204 324)
 )
)
(14
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 97)
  ("(var3 stable)" 97 331)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 99)
  ("(var4 stable)" 99 331)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 74)
  ("(var1 down)" 74 76)
  ("(var1 up)" 76 92)
  ("(var1 stable)" 92 331)
  ("(var2 stable)" 0 83)
  ("(var2 up)" 83 85)
  ("(var2 down)" 85 90)
  ("(var2 stable)" 90 131)
  ("(var2 up)" 131 222)
  ("(var2 stable)" 222 331)
 )
)
(15
 (
  ("(var3 stable)" 0 85)
  ("(var3 down)" 85 87)
  ("(var3 up)" 87 121)
  ("(var3 stable)" 121 365)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 122)
  ("(var4 stable)" 122 365)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 113)
  ("(var1 down)" 113 115)
  ("(var1 up)" 115 117)
  ("(var1 stable)" 117 365)
  ("(var2 stable)" 0 101)
  ("(var2 up)" 101 103)
  ("(var2 down)" 103 108)
  ("(var2 stable)" 108 156)
  ("(var2 up)" 156 224)
  ("(var2 down)" 224 226)
  ("(var2 stable)" 226 365)
 )
)
(16
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 91)
  ("(var3 stable)" 91 307)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 94)
  ("(var4 stable)" 94 307)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 91)
  ("(var1 stable)" 91 307)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 80)
  ("(var2 down)" 80 84)
  ("(var2 up)" 84 218)
  ("(var2 stable)" 218 307)
 )
)
(17
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 63)
  ("(var3 stable)" 63 299)
  ("(var4 stable)" 0 31)
  ("(var4 up)" 31 67)
  ("(var4 stable)" 67 299)
  ("(var1 stable)" 0 30)
  ("(var1 up)" 30 32)
  ("(var1 down)" 32 34)
  ("(var1 up)" 34 66)
  ("(var1 stable)" 66 297)
  ("(var1 down)" 297 299)
  ("(var2 stable)" 0 48)
  ("(var2 up)" 48 50)
  ("(var2 down)" 50 55)
  ("(var2 stable)" 55 99)
  ("(var2 up)" 99 190)
  ("(var2 stable)" 190 299)
 )
)
(18
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 125)
  ("(var3 stable)" 125 350)
  ("(var4 stable)" 0 93)
  ("(var4 up)" 93 120)
  ("(var4 stable)" 120 350)
  ("(var1 stable)" 0 91)
  ("(var1 up)" 91 111)
  ("(var1 stable)" 111 113)
  ("(var1 up)" 113 119)
  ("(var1 stable)" 119 350)
  ("(var2 stable)" 0 105)
  ("(var2 up)" 105 107)
  ("(var2 down)" 107 112)
  ("(var2 up)" 112 227)
  ("(var2 down)" 227 231)
  ("(var2 stable)" 231 350)
 )
)
(19
 (
  ("(var3 stable)" 0 95)
  ("(var3 up)" 95 97)
  ("(var3 down)" 97 99)
  ("(var3 up)" 99 130)
  ("(var3 stable)" 130 387)
  ("(var4 stable)" 0 94)
  ("(var4 up)" 94 132)
  ("(var4 stable)" 132 387)
  ("(var1 stable)" 0 93)
  ("(var1 up)" 93 122)
  ("(var1 stable)" 122 387)
  ("(var2 stable)" 0 110)
  ("(var2 up)" 110 116)
  ("(var2 down)" 116 120)
  ("(var2 up)" 120 259)
  ("(var2 stable)" 259 261)
  ("(var2 up)" 261 263)
  ("(var2 stable)" 263 387)
 )
)
(20
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 100)
  ("(var3 stable)" 100 337)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 101)
  ("(var4 stable)" 101 337)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 78)
  ("(var1 stable)" 78 80)
  ("(var1 up)" 80 96)
  ("(var1 stable)" 96 337)
  ("(var2 down)" 0 2)
  ("(var2 stable)" 2 86)
  ("(var2 up)" 86 88)
  ("(var2 down)" 88 93)
  ("(var2 stable)" 93 135)
  ("(var2 up)" 135 215)
  ("(var2 stable)" 215 337)
 )
)
(21
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 106)
  ("(var3 stable)" 106 345)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 101)
  ("(var4 stable)" 101 345)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 99)
  ("(var1 stable)" 99 345)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 89)
  ("(var2 down)" 89 94)
  ("(var2 stable)" 94 139)
  ("(var2 up)" 139 228)
  ("(var2 stable)" 228 345)
 )
)
(22
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 73)
  ("(var3 stable)" 73 297)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 78)
  ("(var4 stable)" 78 297)
  ("(var1 stable)" 0 50)
  ("(var1 up)" 50 69)
  ("(var1 stable)" 69 297)
  ("(var2 stable)" 0 59)
  ("(var2 up)" 59 61)
  ("(var2 down)" 61 65)
  ("(var2 stable)" 65 100)
  ("(var2 up)" 100 102)
  ("(var2 down)" 102 104)
  ("(var2 up)" 104 179)
  ("(var2 down)" 179 182)
  ("(var2 up)" 182 186)
  ("(var2 stable)" 186 297)
 )
)
(23
 (
  ("(var3 stable)" 0 28)
  ("(var3 up)" 28 56)
  ("(var3 stable)" 56 276)
  ("(var4 stable)" 0 30)
  ("(var4 up)" 30 56)
  ("(var4 stable)" 56 276)
  ("(var1 stable)" 0 28)
  ("(var1 up)" 28 54)
  ("(var1 stable)" 54 276)
  ("(var2 stable)" 0 39)
  ("(var2 down)" 39 41)
  ("(var2 up)" 41 45)
  ("(var2 down)" 45 49)
  ("(var2 stable)" 49 88)
  ("(var2 up)" 88 177)
  ("(var2 stable)" 177 276)
 )
)
(24
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 67)
  ("(var3 stable)" 67 288)
  ("(var4 stable)" 0 29)
  ("(var4 up)" 29 31)
  ("(var4 down)" 31 33)
  ("(var4 up)" 33 67)
  ("(var4 stable)" 67 72)
  ("(var4 up)" 72 76)
  ("(var4 stable)" 76 288)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 65)
  ("(var1 stable)" 65 288)
  ("(var2 stable)" 0 52)
  ("(var2 up)" 52 54)
  ("(var2 down)" 54 62)
  ("(var2 up)" 62 180)
  ("(var2 stable)" 180 288)
 )
)
(25
 (
  ("(var3 stable)" 0 79)
  ("(var3 up)" 79 107)
  ("(var3 stable)" 107 334)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 109)
  ("(var4 stable)" 109 334)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 104)
  ("(var1 stable)" 104 334)
  ("(var2 stable)" 0 93)
  ("(var2 up)" 93 95)
  ("(var2 down)" 95 100)
  ("(var2 stable)" 100 141)
  ("(var2 up)" 141 224)
  ("(var2 stable)" 224 334)
 )
)
(26
 (
  ("(var3 stable)" 0 93)
  ("(var3 up)" 93 95)
  ("(var3 down)" 95 97)
  ("(var3 up)" 97 123)
  ("(var3 stable)" 123 363)
  ("(var4 stable)" 0 94)
  ("(var4 down)" 94 96)
  ("(var4 up)" 96 128)
  ("(var4 stable)" 128 363)
  ("(var1 stable)" 0 95)
  ("(var1 up)" 95 127)
  ("(var1 stable)" 127 363)
  ("(var2 stable)" 0 108)
  ("(var2 up)" 108 110)
  ("(var2 down)" 110 115)
  ("(var2 up)" 115 243)
  ("(var2 stable)" 243 363)
 )
)
(27
 (
  ("(var3 stable)" 0 66)
  ("(var3 up)" 66 94)
  ("(var3 stable)" 94 311)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 95)
  ("(var4 stable)" 95 311)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 94)
  ("(var1 stable)" 94 311)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 89)
  ("(var2 down)" 89 91)
  ("(var2 stable)" 91 116)
  ("(var2 up)" 116 186)
  ("(var2 stable)" 186 188)
  ("(var2 down)" 188 190)
  ("(var2 stable)" 190 311)
 )
)
(28
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 93)
  ("(var3 stable)" 93 325)
  ("(var4 stable)" 0 66)
  ("(var4 up)" 66 94)
  ("(var4 stable)" 94 325)
  ("(var1 stable)" 0 66)
  ("(var1 up)" 66 101)
  ("(var1 stable)" 101 325)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 82)
  ("(var2 down)" 82 87)
  ("(var2 up)" 87 204)
  ("(var2 stable)" 204 325)
 )
)
(29
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 93)
  ("(var3 down)" 93 95)
  ("(var3 stable)" 95 308)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 64)
  ("(var4 stable)" 64 66)
  ("(var4 up)" 66 94)
  ("(var4 stable)" 94 308)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 92)
  ("(var1 stable)" 92 308)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 82)
  ("(var2 down)" 82 87)
  ("(var2 up)" 87 193)
  ("(var2 down)" 193 195)
  ("(var2 up)" 195 202)
  ("(var2 stable)" 202 308)
 )
)
(30
 (
  ("(var3 stable)" 0 65)
  ("(var3 up)" 65 88)
  ("(var3 stable)" 88 90)
  ("(var3 up)" 90 94)
  ("(var3 stable)" 94 96)
  ("(var3 up)" 96 98)
  ("(var3 stable)" 98 313)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 64)
  ("(var4 down)" 64 66)
  ("(var4 up)" 66 98)
  ("(var4 stable)" 98 313)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 91)
  ("(var1 stable)" 91 313)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 81)
  ("(var2 down)" 81 84)
  ("(var2 up)" 84 241)
  ("(var2 stable)" 241 313)
 )
)
(31
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 92)
  ("(var3 stable)" 92 314)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 91)
  ("(var4 stable)" 91 314)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 86)
  ("(var1 stable)" 86 314)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 81)
  ("(var2 down)" 81 83)
  ("(var2 up)" 83 201)
  ("(var2 stable)" 201 314)
 )
)
(32
 (
  ("(var3 stable)" 0 81)
  ("(var3 up)" 81 112)
  ("(var3 stable)" 112 347)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 112)
  ("(var4 stable)" 112 347)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 112)
  ("(var1 stable)" 112 347)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 98)
  ("(var2 down)" 98 103)
  ("(var2 up)" 103 232)
  ("(var2 stable)" 232 347)
 )
)
(33
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 79)
  ("(var3 down)" 79 81)
  ("(var3 up)" 81 110)
  ("(var3 stable)" 110 333)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 113)
  ("(var4 stable)" 113 333)
  ("(var1 stable)" 0 77)
  ("(var1 down)" 77 79)
  ("(var1 up)" 79 105)
  ("(var1 stable)" 105 333)
  ("(var2 stable)" 0 93)
  ("(var2 up)" 93 95)
  ("(var2 down)" 95 100)
  ("(var2 up)" 100 192)
  ("(var2 down)" 192 194)
  ("(var2 up)" 194 204)
  ("(var2 stable)" 204 333)
 )
)
(34
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 73)
  ("(var3 down)" 73 75)
  ("(var3 up)" 75 77)
  ("(var3 stable)" 77 81)
  ("(var3 up)" 81 99)
  ("(var3 stable)" 99 101)
  ("(var3 up)" 101 118)
  ("(var3 stable)" 118 363)
  ("(var4 stable)" 0 82)
  ("(var4 up)" 82 109)
  ("(var4 stable)" 109 363)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 105)
  ("(var1 down)" 105 107)
  ("(var1 up)" 107 112)
  ("(var1 stable)" 112 363)
  ("(var2 stable)" 0 93)
  ("(var2 up)" 93 97)
  ("(var2 down)" 97 101)
  ("(var2 up)" 101 232)
  ("(var2 down)" 232 235)
  ("(var2 stable)" 235 237)
  ("(var2 up)" 237 239)
  ("(var2 stable)" 239 363)
 )
)
(35
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 100)
  ("(var3 stable)" 100 348)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 106)
  ("(var4 down)" 106 108)
  ("(var4 up)" 108 110)
  ("(var4 stable)" 110 348)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 101)
  ("(var1 stable)" 101 348)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 up)" 96 237)
  ("(var2 down)" 237 239)
  ("(var2 stable)" 239 348)
 )
)
(36
 (
  ("(var3 stable)" 0 32)
  ("(var3 up)" 32 66)
  ("(var3 stable)" 66 295)
  ("(var4 stable)" 0 35)
  ("(var4 up)" 35 65)
  ("(var4 stable)" 65 295)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 64)
  ("(var1 stable)" 64 295)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 53)
  ("(var2 down)" 53 58)
  ("(var2 up)" 58 185)
  ("(var2 down)" 185 187)
  ("(var2 up)" 187 189)
  ("(var2 stable)" 189 295)
 )
)
(37
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 107)
  ("(var3 stable)" 107 333)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 80)
  ("(var4 stable)" 80 83)
  ("(var4 up)" 83 114)
  ("(var4 stable)" 114 333)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 105)
  ("(var1 stable)" 105 333)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 96)
  ("(var2 down)" 96 101)
  ("(var2 stable)" 101 139)
  ("(var2 up)" 139 228)
  ("(var2 stable)" 228 333)
 )
)
(38
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 60)
  ("(var3 stable)" 60 62)
  ("(var3 up)" 62 83)
  ("(var3 stable)" 83 310)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 83)
  ("(var4 stable)" 83 310)
  ("(var1 stable)" 0 57)
  ("(var1 up)" 57 79)
  ("(var1 stable)" 79 310)
  ("(var2 stable)" 0 69)
  ("(var2 up)" 69 71)
  ("(var2 down)" 71 76)
  ("(var2 stable)" 76 115)
  ("(var2 up)" 115 176)
  ("(var2 stable)" 176 310)
 )
)
(39
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 75)
  ("(var3 stable)" 75 326)
  ("(var4 stable)" 0 36)
  ("(var4 up)" 36 74)
  ("(var4 stable)" 74 326)
  ("(var1 stable)" 0 47)
  ("(var1 up)" 47 51)
  ("(var1 stable)" 51 53)
  ("(var1 up)" 53 69)
  ("(var1 down)" 69 71)
  ("(var1 stable)" 71 326)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 61)
  ("(var2 down)" 61 66)
  ("(var2 up)" 66 169)
  ("(var2 stable)" 169 171)
  ("(var2 up)" 171 209)
  ("(var2 stable)" 209 326)
 )
)
(40
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 41)
  ("(var3 down)" 41 43)
  ("(var3 up)" 43 65)
  ("(var3 stable)" 65 285)
  ("(var4 stable)" 0 29)
  ("(var4 up)" 29 66)
  ("(var4 stable)" 66 285)
  ("(var1 stable)" 0 43)
  ("(var1 up)" 43 66)
  ("(var1 stable)" 66 285)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 56)
  ("(var2 down)" 56 60)
  ("(var2 up)" 60 153)
  ("(var2 down)" 153 155)
  ("(var2 up)" 155 166)
  ("(var2 stable)" 166 285)
 )
)
(41
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 73)
  ("(var3 down)" 73 76)
  ("(var3 stable)" 76 327)
  ("(var4 stable)" 0 35)
  ("(var4 up)" 35 68)
  ("(var4 stable)" 68 327)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 68)
  ("(var1 stable)" 68 327)
  ("(var2 stable)" 0 56)
  ("(var2 up)" 56 60)
  ("(var2 down)" 60 64)
  ("(var2 up)" 64 198)
  ("(var2 stable)" 198 327)
 )
)
(42
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 84)
  ("(var3 stable)" 84 330)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 54)
  ("(var4 stable)" 54 56)
  ("(var4 up)" 56 90)
  ("(var4 stable)" 90 330)
  ("(var1 up)" 0 2)
  ("(var1 stable)" 2 55)
  ("(var1 up)" 55 82)
  ("(var1 stable)" 82 330)
  ("(var2 stable)" 0 69)
  ("(var2 up)" 69 73)
  ("(var2 down)" 73 77)
  ("(var2 up)" 77 131)
  ("(var2 down)" 131 134)
  ("(var2 up)" 134 191)
  ("(var2 stable)" 191 330)
 )
)
(43
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 79)
  ("(var3 down)" 79 81)
  ("(var3 up)" 81 108)
  ("(var3 stable)" 108 340)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 114)
  ("(var4 down)" 114 116)
  ("(var4 stable)" 116 340)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 108)
  ("(var1 stable)" 108 340)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 96)
  ("(var2 down)" 96 101)
  ("(var2 up)" 101 230)
  ("(var2 down)" 230 233)
  ("(var2 stable)" 233 340)
 )
)
(44
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 53)
  ("(var3 down)" 53 55)
  ("(var3 up)" 55 84)
  ("(var3 stable)" 84 328)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 86)
  ("(var4 stable)" 86 328)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 85)
  ("(var1 stable)" 85 328)
  ("(var2 stable)" 0 68)
  ("(var2 up)" 68 72)
  ("(var2 down)" 72 76)
  ("(var2 up)" 76 219)
  ("(var2 stable)" 219 328)
 )
)
(45
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 77)
  ("(var3 stable)" 77 79)
  ("(var3 up)" 79 81)
  ("(var3 stable)" 81 304)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 82)
  ("(var4 stable)" 82 304)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 81)
  ("(var1 stable)" 81 304)
  ("(var2 stable)" 0 68)
  ("(var2 up)" 68 249)
  ("(var2 stable)" 249 304)
 )
)
(46
 (
  ("(var3 stable)" 0 99)
  ("(var3 up)" 99 131)
  ("(var3 stable)" 131 381)
  ("(var4 up)" 0 2)
  ("(var4 stable)" 2 104)
  ("(var4 up)" 104 136)
  ("(var4 stable)" 136 381)
  ("(var1 stable)" 0 100)
  ("(var1 up)" 100 102)
  ("(var1 stable)" 102 105)
  ("(var1 up)" 105 127)
  ("(var1 stable)" 127 129)
  ("(var1 up)" 129 131)
  ("(var1 stable)" 131 381)
  ("(var2 stable)" 0 116)
  ("(var2 up)" 116 118)
  ("(var2 down)" 118 123)
  ("(var2 up)" 123 223)
  ("(var2 down)" 223 225)
  ("(var2 up)" 225 265)
  ("(var2 stable)" 265 381)
 )
)
(47
 (
  ("(var3 stable)" 0 66)
  ("(var3 up)" 66 97)
  ("(var3 stable)" 97 349)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 66)
  ("(var4 stable)" 66 68)
  ("(var4 up)" 68 90)
  ("(var4 stable)" 90 92)
  ("(var4 up)" 92 94)
  ("(var4 stable)" 94 349)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 97)
  ("(var1 stable)" 97 349)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 81)
  ("(var2 down)" 81 86)
  ("(var2 stable)" 86 131)
  ("(var2 up)" 131 208)
  ("(var2 stable)" 208 349)
 )
)
(48
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 92)
  ("(var3 stable)" 92 340)
  ("(var4 stable)" 0 65)
  ("(var4 up)" 65 89)
  ("(var4 stable)" 89 340)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 90)
  ("(var1 stable)" 90 340)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 up)" 84 209)
  ("(var2 down)" 209 212)
  ("(var2 up)" 212 214)
  ("(var2 stable)" 214 340)
 )
)
(49
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 112)
  ("(var3 stable)" 112 344)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 107)
  ("(var4 stable)" 107 344)
  ("(var1 stable)" 0 85)
  ("(var1 up)" 85 110)
  ("(var1 stable)" 110 344)
  ("(var2 stable)" 0 93)
  ("(var2 up)" 93 95)
  ("(var2 down)" 95 100)
  ("(var2 up)" 100 212)
  ("(var2 down)" 212 214)
  ("(var2 up)" 214 221)
  ("(var2 stable)" 221 344)
 )
)
(50
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 82)
  ("(var3 stable)" 82 335)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 51)
  ("(var4 up)" 51 55)
  ("(var4 stable)" 55 58)
  ("(var4 up)" 58 60)
  ("(var4 stable)" 60 62)
  ("(var4 up)" 62 82)
  ("(var4 stable)" 82 335)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 89)
  ("(var1 stable)" 89 335)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 72)
  ("(var2 down)" 72 77)
  ("(var2 up)" 77 219)
  ("(var2 stable)" 219 335)
 )
)
(51
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 93)
  ("(var3 stable)" 93 306)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 59)
  ("(var4 stable)" 59 61)
  ("(var4 up)" 61 63)
  ("(var4 stable)" 63 65)
  ("(var4 up)" 65 92)
  ("(var4 stable)" 92 306)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 85)
  ("(var1 stable)" 85 306)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 83)
  ("(var2 up)" 83 167)
  ("(var2 down)" 167 170)
  ("(var2 up)" 170 196)
  ("(var2 stable)" 196 306)
 )
)
(52
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 84)
  ("(var3 stable)" 84 334)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 80)
  ("(var4 stable)" 80 83)
  ("(var4 up)" 83 86)
  ("(var4 stable)" 86 334)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 61)
  ("(var1 stable)" 61 63)
  ("(var1 up)" 63 82)
  ("(var1 stable)" 82 334)
  ("(var2 stable)" 0 67)
  ("(var2 up)" 67 71)
  ("(var2 down)" 71 76)
  ("(var2 up)" 76 209)
  ("(var2 stable)" 209 334)
 )
)
(53
 (
  ("(var3 stable)" 0 31)
  ("(var3 up)" 31 72)
  ("(var3 stable)" 72 316)
  ("(var4 stable)" 0 35)
  ("(var4 down)" 35 37)
  ("(var4 up)" 37 64)
  ("(var4 stable)" 64 316)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 40)
  ("(var1 stable)" 40 42)
  ("(var1 up)" 42 65)
  ("(var1 stable)" 65 316)
  ("(var2 stable)" 0 50)
  ("(var2 up)" 50 54)
  ("(var2 down)" 54 57)
  ("(var2 up)" 57 214)
  ("(var2 stable)" 214 316)
 )
)
(54
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 73)
  ("(var3 down)" 73 75)
  ("(var3 stable)" 75 300)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 68)
  ("(var4 stable)" 68 300)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 68)
  ("(var1 down)" 68 71)
  ("(var1 stable)" 71 300)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 56)
  ("(var2 down)" 56 61)
  ("(var2 up)" 61 152)
  ("(var2 down)" 152 154)
  ("(var2 up)" 154 193)
  ("(var2 stable)" 193 300)
 )
)
(55
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 64)
  ("(var3 stable)" 64 290)
  ("(var4 stable)" 0 36)
  ("(var4 up)" 36 70)
  ("(var4 stable)" 70 290)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 65)
  ("(var1 stable)" 65 290)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 53)
  ("(var2 down)" 53 58)
  ("(var2 stable)" 58 91)
  ("(var2 up)" 91 182)
  ("(var2 stable)" 182 290)
 )
)
(56
 (
  ("(var3 stable)" 0 58)
  ("(var3 down)" 58 60)
  ("(var3 up)" 60 95)
  ("(var3 stable)" 95 320)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 90)
  ("(var4 stable)" 90 320)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 84)
  ("(var1 stable)" 84 320)
  ("(var2 stable)" 0 74)
  ("(var2 up)" 74 76)
  ("(var2 down)" 76 81)
  ("(var2 up)" 81 203)
  ("(var2 down)" 203 206)
  ("(var2 stable)" 206 320)
 )
)
(57
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 87)
  ("(var3 stable)" 87 330)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 55)
  ("(var4 stable)" 55 58)
  ("(var4 up)" 58 91)
  ("(var4 stable)" 91 330)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 80)
  ("(var1 stable)" 80 330)
  ("(var2 stable)" 0 71)
  ("(var2 up)" 71 73)
  ("(var2 down)" 73 78)
  ("(var2 up)" 78 172)
  ("(var2 down)" 172 174)
  ("(var2 up)" 174 214)
  ("(var2 stable)" 214 330)
 )
)
(58
 (
  ("(var3 stable)" 0 87)
  ("(var3 up)" 87 113)
  ("(var3 stable)" 113 375)
  ("(var4 stable)" 0 88)
  ("(var4 up)" 88 119)
  ("(var4 stable)" 119 375)
  ("(var1 stable)" 0 83)
  ("(var1 up)" 83 113)
  ("(var1 stable)" 113 375)
  ("(var2 stable)" 0 100)
  ("(var2 up)" 100 102)
  ("(var2 down)" 102 107)
  ("(var2 stable)" 107 155)
  ("(var2 up)" 155 220)
  ("(var2 down)" 220 222)
  ("(var2 up)" 222 229)
  ("(var2 down)" 229 232)
  ("(var2 up)" 232 234)
  ("(var2 stable)" 234 375)
 )
)
(59
 (
  ("(var3 stable)" 0 65)
  ("(var3 up)" 65 94)
  ("(var3 stable)" 94 319)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 94)
  ("(var4 stable)" 94 319)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 89)
  ("(var1 stable)" 89 319)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 up)" 84 202)
  ("(var2 down)" 202 204)
  ("(var2 up)" 204 207)
  ("(var2 stable)" 207 319)
 )
)
(60
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 105)
  ("(var3 stable)" 105 352)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 103)
  ("(var4 stable)" 103 352)
  ("(var1 stable)" 0 76)
  ("(var1 down)" 76 79)
  ("(var1 up)" 79 100)
  ("(var1 stable)" 100 352)
  ("(var2 stable)" 0 90)
  ("(var2 up)" 90 92)
  ("(var2 down)" 92 97)
  ("(var2 up)" 97 199)
  ("(var2 stable)" 199 201)
  ("(var2 up)" 201 210)
  ("(var2 stable)" 210 352)
 )
)
(61
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 95)
  ("(var3 stable)" 95 303)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 92)
  ("(var4 stable)" 92 303)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 90)
  ("(var1 stable)" 90 303)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 81)
  ("(var2 down)" 81 85)
  ("(var2 up)" 85 174)
  ("(var2 stable)" 174 176)
  ("(var2 up)" 176 196)
  ("(var2 stable)" 196 303)
 )
)
(62
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 75)
  ("(var3 stable)" 75 77)
  ("(var3 up)" 77 83)
  ("(var3 stable)" 83 338)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 81)
  ("(var4 stable)" 81 83)
  ("(var4 up)" 83 85)
  ("(var4 stable)" 85 338)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 86)
  ("(var1 down)" 86 88)
  ("(var1 up)" 88 90)
  ("(var1 stable)" 90 338)
  ("(var2 stable)" 0 66)
  ("(var2 up)" 66 70)
  ("(var2 down)" 70 74)
  ("(var2 up)" 74 192)
  ("(var2 stable)" 192 338)
 )
)
(63
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 112)
  ("(var3 stable)" 112 359)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 78)
  ("(var4 stable)" 78 80)
  ("(var4 up)" 80 113)
  ("(var4 stable)" 113 359)
  ("(var1 stable)" 0 89)
  ("(var1 up)" 89 111)
  ("(var1 down)" 111 113)
  ("(var1 stable)" 113 359)
  ("(var2 stable)" 0 99)
  ("(var2 up)" 99 101)
  ("(var2 down)" 101 106)
  ("(var2 up)" 106 207)
  ("(var2 down)" 207 209)
  ("(var2 up)" 209 244)
  ("(var2 stable)" 244 359)
 )
)
(64
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 56)
  ("(var3 stable)" 56 58)
  ("(var3 up)" 58 81)
  ("(var3 stable)" 81 318)
  ("(var4 stable)" 0 54)
  ("(var4 up)" 54 87)
  ("(var4 stable)" 87 318)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 83)
  ("(var1 stable)" 83 318)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 72)
  ("(var2 down)" 72 77)
  ("(var2 up)" 77 171)
  ("(var2 stable)" 171 174)
  ("(var2 up)" 174 203)
  ("(var2 stable)" 203 318)
 )
)
(65
 (
  ("(var3 stable)" 0 62)
  ("(var3 up)" 62 96)
  ("(var3 stable)" 96 328)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 62)
  ("(var4 down)" 62 64)
  ("(var4 up)" 64 95)
  ("(var4 stable)" 95 328)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 91)
  ("(var1 stable)" 91 328)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 80)
  ("(var2 down)" 80 85)
  ("(var2 up)" 85 212)
  ("(var2 stable)" 212 328)
 )
)
(66
 (
  ("(var3 stable)" 0 66)
  ("(var3 up)" 66 104)
  ("(var3 stable)" 104 318)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 77)
  ("(var4 stable)" 77 79)
  ("(var4 up)" 79 98)
  ("(var4 stable)" 98 318)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 99)
  ("(var1 stable)" 99 318)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 90)
  ("(var2 down)" 90 95)
  ("(var2 up)" 95 216)
  ("(var2 stable)" 216 318)
 )
)
(67
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 75)
  ("(var3 stable)" 75 329)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 75)
  ("(var4 stable)" 75 329)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 78)
  ("(var1 stable)" 78 329)
  ("(var2 stable)" 0 61)
  ("(var2 up)" 61 63)
  ("(var2 down)" 63 68)
  ("(var2 stable)" 68 116)
  ("(var2 up)" 116 198)
  ("(var2 down)" 198 202)
  ("(var2 stable)" 202 329)
 )
)
(68
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 84)
  ("(var3 stable)" 84 313)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 49)
  ("(var4 down)" 49 51)
  ("(var4 stable)" 51 53)
  ("(var4 up)" 53 81)
  ("(var4 stable)" 81 313)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 80)
  ("(var1 stable)" 80 313)
  ("(var2 stable)" 0 69)
  ("(var2 up)" 69 71)
  ("(var2 down)" 71 76)
  ("(var2 up)" 76 196)
  ("(var2 stable)" 196 313)
 )
)
(69
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 87)
  ("(var3 stable)" 87 319)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 84)
  ("(var4 stable)" 84 319)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 53)
  ("(var1 stable)" 53 55)
  ("(var1 up)" 55 83)
  ("(var1 stable)" 83 319)
  ("(var2 stable)" 0 64)
  ("(var2 up)" 64 68)
  ("(var2 down)" 68 73)
  ("(var2 stable)" 73 112)
  ("(var2 up)" 112 177)
  ("(var2 stable)" 177 319)
 )
)
(70
 (
  ("(var3 stable)" 0 81)
  ("(var3 down)" 81 83)
  ("(var3 up)" 83 124)
  ("(var3 stable)" 124 361)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 111)
  ("(var4 stable)" 111 361)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 109)
  ("(var1 down)" 109 111)
  ("(var1 stable)" 111 361)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 100)
  ("(var2 down)" 100 104)
  ("(var2 stable)" 104 145)
  ("(var2 up)" 145 148)
  ("(var2 down)" 148 150)
  ("(var2 up)" 150 212)
  ("(var2 down)" 212 214)
  ("(var2 up)" 214 249)
  ("(var2 down)" 249 251)
  ("(var2 up)" 251 253)
  ("(var2 stable)" 253 361)
 )
)
(71
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 111)
  ("(var3 stable)" 111 346)
  ("(var4 stable)" 0 82)
  ("(var4 up)" 82 116)
  ("(var4 stable)" 116 346)
  ("(var1 stable)" 0 85)
  ("(var1 up)" 85 114)
  ("(var1 stable)" 114 346)
  ("(var2 stable)" 0 99)
  ("(var2 up)" 99 101)
  ("(var2 down)" 101 106)
  ("(var2 up)" 106 217)
  ("(var2 down)" 217 219)
  ("(var2 up)" 219 223)
  ("(var2 down)" 223 225)
  ("(var2 up)" 225 227)
  ("(var2 stable)" 227 346)
 )
)
(72
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 58)
  ("(var3 down)" 58 60)
  ("(var3 up)" 60 62)
  ("(var3 stable)" 62 64)
  ("(var3 up)" 64 86)
  ("(var3 stable)" 86 306)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 60)
  ("(var4 stable)" 60 62)
  ("(var4 up)" 62 86)
  ("(var4 stable)" 86 306)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 84)
  ("(var1 stable)" 84 306)
  ("(var2 stable)" 0 75)
  ("(var2 down)" 75 80)
  ("(var2 up)" 80 209)
  ("(var2 stable)" 209 211)
  ("(var2 up)" 211 213)
  ("(var2 stable)" 213 306)
 )
)
(73
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 90)
  ("(var3 stable)" 90 92)
  ("(var3 up)" 92 94)
  ("(var3 stable)" 94 336)
  ("(var4 stable)" 0 50)
  ("(var4 up)" 50 52)
  ("(var4 stable)" 52 57)
  ("(var4 up)" 57 87)
  ("(var4 stable)" 87 336)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 90)
  ("(var1 down)" 90 92)
  ("(var1 up)" 92 94)
  ("(var1 stable)" 94 336)
  ("(var2 stable)" 0 74)
  ("(var2 up)" 74 76)
  ("(var2 down)" 76 81)
  ("(var2 up)" 81 212)
  ("(var2 stable)" 212 336)
 )
)
(74
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 82)
  ("(var3 stable)" 82 300)
  ("(var4 stable)" 0 54)
  ("(var4 up)" 54 85)
  ("(var4 stable)" 85 300)
  ("(var1 stable)" 0 56)
  ("(var1 down)" 56 58)
  ("(var1 up)" 58 80)
  ("(var1 stable)" 80 300)
  ("(var2 stable)" 0 68)
  ("(var2 up)" 68 70)
  ("(var2 down)" 70 74)
  ("(var2 up)" 74 186)
  ("(var2 stable)" 186 300)
 )
)
(75
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 63)
  ("(var3 stable)" 63 282)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 67)
  ("(var4 stable)" 67 282)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 59)
  ("(var1 stable)" 59 282)
  ("(var2 stable)" 0 49)
  ("(var2 up)" 49 51)
  ("(var2 down)" 51 55)
  ("(var2 up)" 55 162)
  ("(var2 stable)" 162 282)
 )
)
(76
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 52)
  ("(var3 down)" 52 54)
  ("(var3 up)" 54 91)
  ("(var3 stable)" 91 327)
  ("(var3 down)" 327 329)
  ("(var4 stable)" 0 54)
  ("(var4 up)" 54 83)
  ("(var4 stable)" 83 329)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 56)
  ("(var1 up)" 56 83)
  ("(var1 stable)" 83 329)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 79)
  ("(var2 up)" 79 216)
  ("(var2 stable)" 216 329)
 )
)
(77
 (
  ("(var3 stable)" 0 41)
  ("(var3 up)" 41 71)
  ("(var3 stable)" 71 316)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 76)
  ("(var4 stable)" 76 316)
  ("(var1 stable)" 0 47)
  ("(var1 up)" 47 69)
  ("(var1 stable)" 69 316)
  ("(var2 stable)" 0 59)
  ("(var2 up)" 59 61)
  ("(var2 down)" 61 66)
  ("(var2 up)" 66 166)
  ("(var2 stable)" 166 168)
  ("(var2 up)" 168 173)
  ("(var2 stable)" 173 316)
 )
)
(78
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 114)
  ("(var3 stable)" 114 359)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 120)
  ("(var4 stable)" 120 359)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 89)
  ("(var1 down)" 89 91)
  ("(var1 up)" 91 114)
  ("(var1 stable)" 114 359)
  ("(var2 stable)" 0 101)
  ("(var2 up)" 101 103)
  ("(var2 down)" 103 108)
  ("(var2 up)" 108 236)
  ("(var2 stable)" 236 359)
 )
)
(79
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 67)
  ("(var3 down)" 67 69)
  ("(var3 up)" 69 71)
  ("(var3 stable)" 71 292)
  ("(var4 stable)" 0 32)
  ("(var4 up)" 32 71)
  ("(var4 stable)" 71 292)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 64)
  ("(var1 stable)" 64 292)
  ("(var2 stable)" 0 53)
  ("(var2 up)" 53 55)
  ("(var2 down)" 55 63)
  ("(var2 up)" 63 162)
  ("(var2 down)" 162 164)
  ("(var2 stable)" 164 292)
 )
)
(80
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 91)
  ("(var3 stable)" 91 93)
  ("(var3 up)" 93 103)
  ("(var3 down)" 103 105)
  ("(var3 stable)" 105 345)
  ("(var4 stable)" 0 66)
  ("(var4 up)" 66 98)
  ("(var4 stable)" 98 345)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 101)
  ("(var1 stable)" 101 345)
  ("(var2 stable)" 0 84)
  ("(var2 up)" 84 86)
  ("(var2 down)" 86 93)
  ("(var2 stable)" 93 134)
  ("(var2 up)" 134 136)
  ("(var2 stable)" 136 139)
  ("(var2 up)" 139 226)
  ("(var2 stable)" 226 345)
 )
)
(81
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 96)
  ("(var3 stable)" 96 338)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 90)
  ("(var4 stable)" 90 338)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 87)
  ("(var1 down)" 87 89)
  ("(var1 stable)" 89 338)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 stable)" 84 128)
  ("(var2 up)" 128 130)
  ("(var2 down)" 130 132)
  ("(var2 up)" 132 216)
  ("(var2 down)" 216 218)
  ("(var2 up)" 218 220)
  ("(var2 stable)" 220 338)
 )
)
(82
 (
  ("(var3 up)" 0 4)
  ("(var3 stable)" 4 57)
  ("(var3 up)" 57 59)
  ("(var3 down)" 59 61)
  ("(var3 up)" 61 89)
  ("(var3 stable)" 89 350)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 85)
  ("(var4 stable)" 85 350)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 91)
  ("(var1 stable)" 91 350)
  ("(var2 stable)" 0 75)
  ("(var2 up)" 75 79)
  ("(var2 down)" 79 83)
  ("(var2 stable)" 83 129)
  ("(var2 up)" 129 220)
  ("(var2 stable)" 220 350)
 )
)
(83
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 95)
  ("(var3 down)" 95 97)
  ("(var3 up)" 97 99)
  ("(var3 stable)" 99 332)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 95)
  ("(var4 stable)" 95 332)
  ("(var1 stable)" 0 66)
  ("(var1 up)" 66 92)
  ("(var1 stable)" 92 332)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 82)
  ("(var2 down)" 82 87)
  ("(var2 up)" 87 207)
  ("(var2 down)" 207 209)
  ("(var2 stable)" 209 332)
 )
)
(84
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 71)
  ("(var3 stable)" 71 308)
  ("(var4 stable)" 0 41)
  ("(var4 down)" 41 43)
  ("(var4 up)" 43 75)
  ("(var4 stable)" 75 308)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 40)
  ("(var1 down)" 40 42)
  ("(var1 up)" 42 74)
  ("(var1 stable)" 74 308)
  ("(var2 stable)" 0 55)
  ("(var2 up)" 55 57)
  ("(var2 down)" 57 62)
  ("(var2 stable)" 62 107)
  ("(var2 up)" 107 196)
  ("(var2 stable)" 196 308)
 )
)
(85
 (
  ("(var3 stable)" 0 90)
  ("(var3 up)" 90 119)
  ("(var3 stable)" 119 366)
  ("(var4 stable)" 0 88)
  ("(var4 up)" 88 90)
  ("(var4 down)" 90 92)
  ("(var4 up)" 92 120)
  ("(var4 stable)" 120 366)
  ("(var1 stable)" 0 91)
  ("(var1 up)" 91 93)
  ("(var1 down)" 93 95)
  ("(var1 up)" 95 98)
  ("(var1 stable)" 98 100)
  ("(var1 up)" 100 115)
  ("(var1 stable)" 115 117)
  ("(var1 up)" 117 121)
  ("(var1 stable)" 121 366)
  ("(var2 stable)" 0 105)
  ("(var2 up)" 105 109)
  ("(var2 down)" 109 113)
  ("(var2 up)" 113 159)
  ("(var2 stable)" 159 161)
  ("(var2 up)" 161 238)
  ("(var2 stable)" 238 240)
  ("(var2 up)" 240 243)
  ("(var2 stable)" 243 366)
 )
)
(86
 (
  ("(var3 stable)" 0 41)
  ("(var3 up)" 41 75)
  ("(var3 stable)" 75 322)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 59)
  ("(var4 stable)" 59 61)
  ("(var4 up)" 61 80)
  ("(var4 stable)" 80 322)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 42)
  ("(var1 down)" 42 44)
  ("(var1 up)" 44 74)
  ("(var1 stable)" 74 322)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 63)
  ("(var2 down)" 63 67)
  ("(var2 up)" 67 198)
  ("(var2 stable)" 198 322)
 )
)
(87
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 88)
  ("(var3 stable)" 88 339)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 87)
  ("(var4 stable)" 87 339)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 88)
  ("(var1 stable)" 88 339)
  ("(var2 stable)" 0 69)
  ("(var2 up)" 69 71)
  ("(var2 down)" 71 76)
  ("(var2 up)" 76 217)
  ("(var2 stable)" 217 339)
 )
)
(88
 (
  ("(var3 stable)" 0 41)
  ("(var3 up)" 41 80)
  ("(var3 stable)" 80 316)
  ("(var4 up)" 0 5)
  ("(var4 stable)" 5 38)
  ("(var4 up)" 38 82)
  ("(var4 stable)" 82 316)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 78)
  ("(var1 stable)" 78 316)
  ("(var2 stable)" 0 60)
  ("(var2 up)" 60 62)
  ("(var2 down)" 62 67)
  ("(var2 stable)" 67 116)
  ("(var2 up)" 116 203)
  ("(var2 stable)" 203 316)
 )
)
(89
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 118)
  ("(var3 stable)" 118 331)
  ("(var4 stable)" 0 81)
  ("(var4 up)" 81 111)
  ("(var4 stable)" 111 331)
  ("(var1 stable)" 0 82)
  ("(var1 up)" 82 85)
  ("(var1 down)" 85 88)
  ("(var1 up)" 88 107)
  ("(var1 stable)" 107 331)
  ("(var2 stable)" 0 98)
  ("(var2 up)" 98 100)
  ("(var2 down)" 100 105)
  ("(var2 up)" 105 194)
  ("(var2 stable)" 194 196)
  ("(var2 up)" 196 233)
  ("(var2 stable)" 233 331)
 )
)
(90
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 113)
  ("(var3 stable)" 113 358)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 118)
  ("(var4 stable)" 118 358)
  ("(var1 stable)" 0 83)
  ("(var1 up)" 83 85)
  ("(var1 stable)" 85 88)
  ("(var1 up)" 88 113)
  ("(var1 stable)" 113 358)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 100)
  ("(var2 down)" 100 104)
  ("(var2 stable)" 104 146)
  ("(var2 up)" 146 238)
  ("(var2 stable)" 238 358)
 )
)
(91
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 75)
  ("(var3 stable)" 75 296)
  ("(var4 stable)" 0 35)
  ("(var4 up)" 35 73)
  ("(var4 stable)" 73 296)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 73)
  ("(var1 stable)" 73 296)
  ("(var2 stable)" 0 60)
  ("(var2 up)" 60 62)
  ("(var2 down)" 62 67)
  ("(var2 up)" 67 180)
  ("(var2 stable)" 180 296)
 )
)
(92
 (
  ("(var3 stable)" 0 52)
  ("(var3 up)" 52 86)
  ("(var3 stable)" 86 328)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 87)
  ("(var4 stable)" 87 328)
  ("(var1 stable)" 0 44)
  ("(var1 up)" 44 83)
  ("(var1 stable)" 83 328)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 72)
  ("(var2 down)" 72 77)
  ("(var2 up)" 77 175)
  ("(var2 down)" 175 177)
  ("(var2 up)" 177 204)
  ("(var2 stable)" 204 328)
 )
)
(93
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 72)
  ("(var3 down)" 72 74)
  ("(var3 up)" 74 117)
  ("(var3 stable)" 117 363)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 104)
  ("(var4 down)" 104 106)
  ("(var4 up)" 106 108)
  ("(var4 stable)" 108 363)
  ("(var1 stable)" 0 81)
  ("(var1 up)" 81 105)
  ("(var1 stable)" 105 363)
  ("(var2 stable)" 0 91)
  ("(var2 up)" 91 97)
  ("(var2 down)" 97 101)
  ("(var2 up)" 101 221)
  ("(var2 stable)" 221 363)
 )
)
(94
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 93)
  ("(var3 stable)" 93 344)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 91)
  ("(var4 stable)" 91 344)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 63)
  ("(var1 down)" 63 65)
  ("(var1 up)" 65 68)
  ("(var1 down)" 68 70)
  ("(var1 up)" 70 92)
  ("(var1 stable)" 92 344)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 78)
  ("(var2 down)" 78 83)
  ("(var2 up)" 83 173)
  ("(var2 down)" 173 175)
  ("(var2 up)" 175 202)
  ("(var2 down)" 202 205)
  ("(var2 up)" 205 207)
  ("(var2 down)" 207 209)
  ("(var2 stable)" 209 344)
 )
)
(95
 (
  ("(var3 stable)" 0 2)
  ("(var3 down)" 2 4)
  ("(var3 stable)" 4 36)
  ("(var3 up)" 36 38)
  ("(var3 stable)" 38 42)
  ("(var3 up)" 42 71)
  ("(var3 stable)" 71 315)
  ("(var4 up)" 0 2)
  ("(var4 down)" 2 5)
  ("(var4 stable)" 5 37)
  ("(var4 up)" 37 72)
  ("(var4 stable)" 72 315)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 74)
  ("(var1 stable)" 74 315)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 57)
  ("(var2 down)" 57 61)
  ("(var2 up)" 61 213)
  ("(var2 stable)" 213 315)
 )
)
(96
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 79)
  ("(var3 stable)" 79 81)
  ("(var3 up)" 81 107)
  ("(var3 stable)" 107 364)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 108)
  ("(var4 stable)" 108 364)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 101)
  ("(var1 down)" 101 103)
  ("(var1 up)" 103 105)
  ("(var1 stable)" 105 364)
  ("(var2 stable)" 0 90)
  ("(var2 up)" 90 94)
  ("(var2 down)" 94 98)
  ("(var2 up)" 98 211)
  ("(var2 stable)" 211 214)
  ("(var2 up)" 214 219)
  ("(var2 stable)" 219 364)
 )
)
(97
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 73)
  ("(var3 stable)" 73 307)
  ("(var4 stable)" 0 35)
  ("(var4 up)" 35 74)
  ("(var4 stable)" 74 307)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 69)
  ("(var1 stable)" 69 307)
  ("(var2 stable)" 0 60)
  ("(var2 up)" 60 62)
  ("(var2 down)" 62 67)
  ("(var2 up)" 67 157)
  ("(var2 down)" 157 159)
  ("(var2 up)" 159 192)
  ("(var2 stable)" 192 307)
 )
)
(98
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 87)
  ("(var3 stable)" 87 327)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 83)
  ("(var4 stable)" 83 327)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 83)
  ("(var1 down)" 83 85)
  ("(var1 stable)" 85 327)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 74)
  ("(var2 down)" 74 78)
  ("(var2 stable)" 78 122)
  ("(var2 up)" 122 176)
  ("(var2 down)" 176 178)
  ("(var2 up)" 178 182)
  ("(var2 stable)" 182 186)
  ("(var2 up)" 186 217)
  ("(var2 down)" 217 220)
  ("(var2 up)" 220 223)
  ("(var2 stable)" 223 327)
 )
)
(99
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 108)
  ("(var3 stable)" 108 320)
  ("(var4 stable)" 0 82)
  ("(var4 up)" 82 117)
  ("(var4 stable)" 117 320)
  ("(var1 stable)" 0 85)
  ("(var1 up)" 85 108)
  ("(var1 stable)" 108 320)
  ("(var2 stable)" 0 98)
  ("(var2 up)" 98 100)
  ("(var2 down)" 100 105)
  ("(var2 up)" 105 222)
  ("(var2 stable)" 222 320)
 )
)
(100
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 77)
  ("(var3 down)" 77 79)
  ("(var3 up)" 79 82)
  ("(var3 stable)" 82 309)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 77)
  ("(var4 stable)" 77 309)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 76)
  ("(var1 down)" 76 78)
  ("(var1 up)" 78 80)
  ("(var1 stable)" 80 309)
  ("(var2 stable)" 0 62)
  ("(var2 up)" 62 64)
  ("(var2 down)" 64 69)
  ("(var2 up)" 69 207)
  ("(var2 stable)" 207 309)
 )
)
